\begin{tabbing}
ESMachineAxiom($E$;$T$;$V$;$M$;${\it loc}$;${\it knd}$;${\it val}$;
\\[0ex]${\it when}$;${\it after}$;
\\[0ex]${\it sndr}$;${\it Trans}$;${\it Send}$;${\it Choose}$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=($\forall$$e$:$E$. ($\lambda$$x$.${\it after}$($x$,$e$)) = ${\it Trans}$(${\it loc}$($e$),${\it knd}$($e$),${\it val}$($e$),$\lambda$$x$.${\it when}$($x$,$e$)))\+
\\[0ex]\& (\=$\forall$$e$:$E$.\+
\\[0ex]($\uparrow$islocal(${\it knd}$($e$)))
\\[0ex]$\Rightarrow$ \=(($\uparrow$isl(${\it Choose}$(${\it loc}$($e$),act(${\it knd}$($e$)),$\lambda$$x$.${\it when}$($x$,$e$))))\+
\\[0ex]c$\wedge$ (${\it val}$($e$) = outl(${\it Choose}$(${\it loc}$($e$),act(${\it knd}$($e$)),$\lambda$$x$.${\it when}$($x$,$e$))))))
\-\-\\[0ex]\& (\=$\forall$$e$:$E$.\+
\\[0ex]($\uparrow$isrcv(${\it knd}$($e$)))
\\[0ex]$\Rightarrow$ ($<$lnk(${\it knd}$($e$)), tag(${\it knd}$($e$)), ${\it val}$($e$)$>$ $\in$ \=${\it Send}$\+
\\[0ex](${\it loc}$(${\it sndr}$($e$))
\\[0ex],${\it knd}$(${\it sndr}$($e$))
\\[0ex],${\it val}$(${\it sndr}$($e$))
\\[0ex],$\lambda$$x$.${\it when}$($x$,${\it sndr}$($e$)))))
\-\-\-
\end{tabbing}